1987 sept 12

I need to make progress in turning conceptual problems into technical
problems.  It seems likely that I can do this with the problem of
giving priority to the normality of what is known over the normality
of that which is derived from it.  The example of beating the defaults
of American women by facts derived from the fact that the woman is a
particular person's mother looks good.

¬ab aspect1 x ⊃ race mother x = race x

race Sam = white

¬ab aspect2 z ⊃ race z = yellow

This gives a conflict, so we need to reify enough to express the priority
that what we know about someone's mother as derived from what we know
about him takes precedence over defaults on the person.

Maybe we need some more reified entities --- for example, "all I know about X".

1987 Sept 20

Do a good job of formalizing set theory within set theory, i.e.
introducing the formulas of first order logic and set theory
as objects, formalizing interpretations and satisfaction,
reaching the goal of asserting the existence of internal models.

This goal is related to the goal of heavy duty set theory (hdst).
The latter requires being able to include arbitrary Lisp Machine
objects as members of sets, especially to be able to form finite sets
of such objects by listing them.

1987 Sept 26

Enthusiasms

	It seems that arbitrarily intelligent people can fall victim
to enthusiasms.  The sharpest examples occur when, before succumbing,
the individual can give the same arguments against the enthusiasm
that he will later regard as decisive when he recovers from it.

The two examples worth treating are Hitlerism and 1960s leftism.
Putnam may do for a victim of the latter, and there should be all
sorts of smart people who would do for the former.  Ask Teller for
examples.

Declarative expression of reasoning heuristics

1. Use elephant in the expression of the heuristics, i.e. allow
reference to past beliefs and inferences.  In particular, we can
allow rules of the form "do X if it hasn't already been done".

2. good-to-apply(rule, data, s)

3. goal(show(congruent(tri1,tri2)),s) ∧
have(equal(side(AB,tri1),side(AB,tri2)),s) ∧
have(equal(side(AC,tri1),side(AC,tri2)),s) ⊃
goal1(show(equal(angle(A,tri1),angle(A,tri2)),s)

This is true, but we need some way of saying that this
should be tried before trying to prove some other
instantiation of side-angle-side for which we don't
have two of the premisses already.

1987 Sept 27

The Lisp machine doesn't have the equivalent of preview.  You
can find out what a command does in general using HELP, but
you can't find out what a particular instantiation would do.

It also doesn't seem to have the ability to include comments
in DIRED.

Is it really true that ZMACS has no c-J?

1987 sept 28

emphasize that the boat can be presumed to be usable because
it is there for a purpose.

Can we have the clarity of the Peirera-Porto coloring program
without its presumptive algorithm?

In order to prove that something cannot happen, we need to
enumerate possible events and prove that each of them
preserves a predicate incompatible with what we want to
prove cannot happen.  However, there is a simpler case of
prevention.  When A grabs B to prevent him from walking in
front of a car, he isn't saving B forever from being run
over, he is just preventing a particular event.  Include
prevention in the situation calculus discussion in class,
especially contrasting it with STRIPS, Prolog and other purely
computational formalisms.

Distinguish purely computational formalisms.

1987 Oct 4

It seems we cannot avoid designating some terms as primitive in
order to make frames.  However, we can make the designations
of what is primitive context-dependent.

1987 Oct 5

In a general editor, clearly named pieces of text should play a
primary role.  EMACS's one character registers are likely to lead
to trouble.

However, it may be that the general item should be a text with
imbedded variables.  We can then substitute for these variables.

Still more general is a -expression with some free variables.
The result of substituting that for a variable is unclear.

****

What computations can be verified by a finite state machine -
with one head? - with two heads?  With two heads one can
obviously verify that two unary numbers are equal and not
with one head.  With three heads one can keep one on a sequence
of instructions.  John Cocke may have a view on this.

****

The following is related to the non-monotonic reasoning required
for the Yale shooting problem but by a chain of steps that may
be tenuous.  Our current approach involves reifying reasons and
saying that nothing occurs without a reason.  Shooting is a reason
for dying, though not a conclusive one, but there is no reason for
the gun to become unloaded.  (This is especially true if the
Yale shooting scenario is a story or a plan).  I worried that
our intuitive view of this may bog down when we try to formalize
it, because this intuitive view is founded on looking at the
database from the outside, i.e. have sentences that aren't in
the database but meta to it.

Trying to invent suitable predicates and functions of databases
has been frustrating, and the following is a conjecture of why
and what might be done about it.

Suppose the basic object isn't just the database but the database
+ metalinguistic commentary.  The predicates on databases refer
to the commentary as well as to the database itself.

Note: {p,p∧q} has the same extension as {p∧q} but isn't the same
database, because there may be operations that work on the
separated  p.  {p,q} is clearer, because it suggests that  p  and
q  can be modified separately.

One kind of commentary is derivation information, e.g. that  q
came from  p  and  p ⊃ q by modus ponens.

****

Let's think about an Elephant Prolog that only adds to its database,
and everything in it remains true.  However, some of the information
initially and also deduced is meta-information.  All of Prolog's
hidden information, e.g. goal and proof trees, are to be explicit
meta-information.

Such a system might record stages, e.g. by successively proving
is-stage(0), is-stage(1), etc.  Meta-sentences may have stage
arguments and can thus assert what isn't known at a given stage.
Everything deduced is eternally true.  The deduction routines
pay attention to what stage has been reached.  They may have
negative premisses about what has been deduced, and this somehow
suggests that we try to make them get by with negation as failure.

Maybe Apt will be interested in this.

Oct 8

Elephant logic

The axioms are such that all results of inference include their history.
The simplest kind of axiom that works for this is

b(p,r1) ∧ b(p imp q,r2) ⊃ b(q,mp(p,q,r1,r2)).

However, this doesn't contain enough information about the state
of the database to do non-monotonic reasoning.  For this we need
the database as a parameter and axioms that describe how it changes.

holds(p,r1,db) ∧ holds(p imp q,r2,db) ⊃ holds(q,mp(p,q,r1,r2),result(mp(p,q,r1,r2),db))

We also require

holds(p,r,db) ⊃ holds(p,r,result(mp(x,y,z,w),db))

which expresses the monotonicity of modus ponens.

In order to get an example of non-monotonicity, it seems easiest to
take an example from default logic.

rule(name(p,Mq,r),db) ∧ holds(p,r1,db) ∧ consistent(q,db) ⊃
	holds(r,default(name,p,q,r),r1),result(default(name(p,q,r),r1),db)).

See elephant-logic.text for more.

Oct 8

What are the functional requirements for communication?  This is
the question the linguists fail to treat.  These requirements
involve the knowledge of the sender and recipient including linguistic
knowledge.

Oct 9

isrel(s)

is a predicate on situation, to be minimized in some way, that
tells what situations we are interested in.  We might have

isrel s0 ∧ isrel result(load,s0) ∧ isrel(load*wait,s0) ∧ 
	isrel(load*wait*shoot,s0)

and circumscribe  ab  only over the relevant situations.

Oct 10

Types

	This may be in Jussi's plan for the new EKL already.  It is
undesirable to declare the type of anything.  However, when the symbol
f  is applied to the symbol  x,  then a type equation is induced saying
that the type of  f  is applicable to the type of  x.  At any time one
may ask about type consistency, and then the type equations that have
been induced by usage are checked for consistency.  We can even allow
the derivation of Russell's paradox.  It is allowed, but when we next
check for type consistency, the system backtracks until it comes to
the last point at which type consistency existed, kills the step that
spoiled consistency and everything that follows from it.

Nov 1

	The psychological tendencies of humans that made for tribal
behavior exist in present humans, especially adolescents and young
adults.  Trigger: UTexas locks the doors on buildings during home
game Saturdays, perhaps this is based on experience.  Maybe fans of
the other team have a tribal tendency to take trophies.  Non-sequitur:
and women.  Women are taken by tribal raiders and partly acquiesce,
especially if they have already come to the opinion: there are no
interesting young men around here.  I conjecture that this is a
conclusion young women often reach.  It accounts for migration to
the cities, preference for distant colleges.

Nov 7
	Problem (forgot)

Nov 28
	The elephant language should have sequences of times as
objects so it can be used to program the pay of a modal logician.
We may also want what might be called Zeno's axiom.  All sequences
of times are finite.  It is an induction schema over such sequences.

Nov 30
	R. Abelson's theory of salience may have application to more
than elections.  The point of the theory is that it is easier to change
the salience of an issue to a person than to change his opinion of the
issue.  Tar Baby is intended to increase the salience of the
desirability of separating physics from politics to the American
Physical Society.

	Napoleon said that one should not interrupt an enemy when he
is making a mistake.  Does this apply to the potential North trial?
A lot depends on the likely judge.

	When a hostage is about to be released in Beirut, a sound truck
should go through the city playing a variety of tunes recognizable by
the hostage.  Otherwise, airplanes can fly over a given area on a given
day simultaneously with a radio announcement of a sort that the captors
are likely to tell the hostage about.

Dec 11
	Entries in the Yellow Pages should be coded to map co-ordinates,
perhaps of the A12 sort in most city maps but perhaps co-ordinated to
latitude and longitude in preparation for the widespread availability of
GPS.

	A lock that accepts ordinary Yale keys but is programmed which
keys to accept.  A fancy version can read and  record the keys submitted
to it.

VAL's proposals on chronological minimization:

ab < ab' ≡ ∃t0[¬ab(t0) ∧ ab'(t0) ∧ ∀t(t < t0 ⊃ ab(t) ≡ ab'(t))]

ab ≤ ab' ≡ ∃t0 ∀s[(time(s) < t0 ⊃ (ab(s) ≡ ab'(s))) ∧ ((time(s) ≥ t0 ∧ ab(s)) ⊃ ab'(s))]

Dec 28 - from inventions file of Nov 7
micro-clipboard, dress pack